$M$.init($x$,$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(IdDeq; (($M$.2.2).1); $x$; $a$,$x_{0}$.($v$ = $x_{0}$ $\in$ $\mathbb{Q}\rightarrow$fpf{-}cap($M$.1;IdDeq;$x$;Void)))